The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

cond1(true, x, y, z) → cond2(gr(y, z), x, y, z)
cond2(true, x, y, z) → cond2(gr(y, z), p(x), p(y), z)
cond2(false, x, y, z) → cond1(and(eq(x, y), gr(x, z)), x, y, z)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

cond1(true, x, y, z) → cond2(gr(y, z), x, y, z) [1]
cond2(true, x, y, z) → cond2(gr(y, z), p(x), p(y), z) [1]
cond2(false, x, y, z) → cond1(and(eq(x, y), gr(x, z)), x, y, z) [1]
gr(0, x) → false [1]
gr(s(x), 0) → true [1]
gr(s(x), s(y)) → gr(x, y) [1]
p(0) → 0 [1]
p(s(x)) → x [1]
eq(0, 0) → true [1]
eq(s(x), 0) → false [1]
eq(0, s(x)) → false [1]
eq(s(x), s(y)) → eq(x, y) [1]
and(true, true) → true [1]
and(false, x) → false [1]
and(x, false) → false [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

cond1(true, x, y, z) → cond2(gr(y, z), x, y, z) [1]
cond2(true, x, y, z) → cond2(gr(y, z), p(x), p(y), z) [1]
cond2(false, x, y, z) → cond1(and(eq(x, y), gr(x, z)), x, y, z) [1]
gr(0, x) → false [1]
gr(s(x), 0) → true [1]
gr(s(x), s(y)) → gr(x, y) [1]
p(0) → 0 [1]
p(s(x)) → x [1]
eq(0, 0) → true [1]
eq(s(x), 0) → false [1]
eq(0, s(x)) → false [1]
eq(s(x), s(y)) → eq(x, y) [1]
and(true, true) → true [1]
and(false, x) → false [1]
and(x, false) → false [1]

The TRS has the following type information:

cond1 :: true:false → 0:s → 0:s → 0:s → cond1:cond2 true :: true:false cond2 :: true:false → 0:s → 0:s → 0:s → cond1:cond2 gr :: 0:s → 0:s → true:false p :: 0:s → 0:s false :: true:false and :: true:false → true:false → true:false eq :: 0:s → 0:s → true:false 0 :: 0:s s :: 0:s → 0:s

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

cond1(v0, v1, v2, v3) → null_cond1 [0]

And the following fresh constants:

null_cond1

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: cond1(true, x, y, z) → cond2(gr(y, z), x, y, z) [1] cond2(true, x, y, z) → cond2(gr(y, z), p(x), p(y), z) [1] cond2(false, x, y, z) → cond1(and(eq(x, y), gr(x, z)), x, y, z) [1] gr(0, x) → false [1] gr(s(x), 0) → true [1] gr(s(x), s(y)) → gr(x, y) [1] p(0) → 0 [1] p(s(x)) → x [1] eq(0, 0) → true [1] eq(s(x), 0) → false [1] eq(0, s(x)) → false [1] eq(s(x), s(y)) → eq(x, y) [1] and(true, true) → true [1] and(false, x) → false [1] and(x, false) → false [1] cond1(v0, v1, v2, v3) → null_cond1 [0] The TRS has the following type information: cond1 :: true:false → 0:s → 0:s → 0:s → null_cond1 true :: true:false cond2 :: true:false → 0:s → 0:s → 0:s → null_cond1 gr :: 0:s → 0:s → true:false p :: 0:s → 0:s false :: true:false and :: true:false → true:false → true:false eq :: 0:s → 0:s → true:false 0 :: 0:s s :: 0:s → 0:s null_cond1 :: null_cond1 Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

true => 1
false => 0
0 => 0
null_cond1 => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

and(z', z'') -{ 1 }→ 1 :|: z' = 1, z'' = 1
and(z', z'') -{ 1 }→ 0 :|: x >= 0, z'' = x, z' = 0
and(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' = x, x >= 0
cond1(z', z'', z1, z2) -{ 1 }→ cond2(gr(y, z), x, y, z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
cond1(z', z'', z1, z2) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, v3 >= 0, z' = v0
cond2(z', z'', z1, z2) -{ 1 }→ cond2(gr(y, z), p(x), p(y), z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
cond2(z', z'', z1, z2) -{ 1 }→ cond1(and(eq(x, y), gr(x, z)), x, y, z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 0
eq(z', z'') -{ 1 }→ eq(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
eq(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 0
eq(z', z'') -{ 1 }→ 0 :|: z'' = 0, z' = 1 + x, x >= 0
eq(z', z'') -{ 1 }→ 0 :|: x >= 0, z'' = 1 + x, z' = 0
gr(z', z'') -{ 1 }→ gr(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
gr(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 1 + x, x >= 0
gr(z', z'') -{ 1 }→ 0 :|: x >= 0, z'' = x, z' = 0
p(z') -{ 1 }→ x :|: z' = 1 + x, x >= 0
p(z') -{ 1 }→ 0 :|: z' = 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V2, V3),0,[cond1(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3),0,[cond2(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3),0,[gr(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[p(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[eq(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[and(V, V1, Out)],[V >= 0,V1 >= 0]). eq(cond1(V, V1, V2, V3, Out),1,[gr(V4, V5, Ret0),cond2(Ret0, V6, V4, V5, Ret)],[Out = Ret,V2 = V4,V5 >= 0,V3 = V5,V6 >= 0,V4 >= 0,V1 = V6,V = 1]). eq(cond2(V, V1, V2, V3, Out),1,[gr(V7, V8, Ret01),p(V9, Ret1),p(V7, Ret2),cond2(Ret01, Ret1, Ret2, V8, Ret3)],[Out = Ret3,V2 = V7,V8 >= 0,V3 = V8,V9 >= 0,V7 >= 0,V1 = V9,V = 1]). eq(cond2(V, V1, V2, V3, Out),1,[eq(V10, V11, Ret00),gr(V10, V12, Ret011),and(Ret00, Ret011, Ret02),cond1(Ret02, V10, V11, V12, Ret4)],[Out = Ret4,V2 = V11,V12 >= 0,V3 = V12,V10 >= 0,V11 >= 0,V1 = V10,V = 0]). eq(gr(V, V1, Out),1,[],[Out = 0,V13 >= 0,V1 = V13,V = 0]). eq(gr(V, V1, Out),1,[],[Out = 1,V1 = 0,V = 1 + V14,V14 >= 0]). eq(gr(V, V1, Out),1,[gr(V15, V16, Ret5)],[Out = Ret5,V = 1 + V15,V15 >= 0,V16 >= 0,V1 = 1 + V16]). eq(p(V, Out),1,[],[Out = 0,V = 0]). eq(p(V, Out),1,[],[Out = V17,V = 1 + V17,V17 >= 0]). eq(eq(V, V1, Out),1,[],[Out = 1,V1 = 0,V = 0]). eq(eq(V, V1, Out),1,[],[Out = 0,V1 = 0,V = 1 + V18,V18 >= 0]). eq(eq(V, V1, Out),1,[],[Out = 0,V19 >= 0,V1 = 1 + V19,V = 0]). eq(eq(V, V1, Out),1,[eq(V20, V21, Ret6)],[Out = Ret6,V = 1 + V20,V20 >= 0,V21 >= 0,V1 = 1 + V21]). eq(and(V, V1, Out),1,[],[Out = 1,V = 1,V1 = 1]). eq(and(V, V1, Out),1,[],[Out = 0,V22 >= 0,V1 = V22,V = 0]). eq(and(V, V1, Out),1,[],[Out = 0,V1 = 0,V = V23,V23 >= 0]). eq(cond1(V, V1, V2, V3, Out),0,[],[Out = 0,V3 = V24,V25 >= 0,V2 = V26,V27 >= 0,V1 = V27,V26 >= 0,V24 >= 0,V = V25]). input_output_vars(cond1(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(cond2(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(gr(V,V1,Out),[V,V1],[Out]). input_output_vars(p(V,Out),[V],[Out]). input_output_vars(eq(V,V1,Out),[V,V1],[Out]). input_output_vars(and(V,V1,Out),[V,V1],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. non_recursive : [and/3]
1. recursive : [eq/3]
2. recursive : [gr/3]
3. non_recursive : [p/2]
4. recursive : [cond1/5,cond2/5]
5. non_recursive : [start/4]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into and/3
1. SCC is partially evaluated into eq/3
2. SCC is partially evaluated into gr/3
3. SCC is partially evaluated into p/2
4. SCC is partially evaluated into cond2/5
5. SCC is partially evaluated into start/4

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations and/3
* CE 23 is refined into CE [24]
* CE 21 is refined into CE [25]
* CE 22 is refined into CE [26]


### Cost equations --> "Loop" of and/3
* CEs [24] --> Loop 17
* CEs [25] --> Loop 18
* CEs [26] --> Loop 19

### Ranking functions of CR and(V,V1,Out)

#### Partial ranking functions of CR and(V,V1,Out)


### Specialization of cost equations eq/3
* CE 20 is refined into CE [27]
* CE 18 is refined into CE [28]
* CE 19 is refined into CE [29]
* CE 17 is refined into CE [30]


### Cost equations --> "Loop" of eq/3
* CEs [28] --> Loop 20
* CEs [29] --> Loop 21
* CEs [30] --> Loop 22
* CEs [27] --> Loop 23

### Ranking functions of CR eq(V,V1,Out)
* RF of phase [23]: [V,V1]

#### Partial ranking functions of CR eq(V,V1,Out)
* Partial RF of phase [23]:
- RF of loop [23:1]:
V
V1


### Specialization of cost equations gr/3
* CE 11 is refined into CE [31]
* CE 10 is refined into CE [32]
* CE 9 is refined into CE [33]


### Cost equations --> "Loop" of gr/3
* CEs [32] --> Loop 24
* CEs [33] --> Loop 25
* CEs [31] --> Loop 26

### Ranking functions of CR gr(V,V1,Out)
* RF of phase [26]: [V,V1]

#### Partial ranking functions of CR gr(V,V1,Out)
* Partial RF of phase [26]:
- RF of loop [26:1]:
V
V1


### Specialization of cost equations p/2
* CE 16 is refined into CE [34]
* CE 15 is refined into CE [35]


### Cost equations --> "Loop" of p/2
* CEs [34] --> Loop 27
* CEs [35] --> Loop 28

### Ranking functions of CR p(V,Out)

#### Partial ranking functions of CR p(V,Out)


### Specialization of cost equations cond2/5
* CE 14 is refined into CE [36,37,38,39,40,41,42,43]
* CE 13 is refined into CE [44,45]
* CE 12 is refined into CE [46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63]


### Cost equations --> "Loop" of cond2/5
* CEs [56] --> Loop 29
* CEs [58,59] --> Loop 30
* CEs [60] --> Loop 31
* CEs [54,55] --> Loop 32
* CEs [63] --> Loop 33
* CEs [62] --> Loop 34
* CEs [57] --> Loop 35
* CEs [53] --> Loop 36
* CEs [61] --> Loop 37
* CEs [52] --> Loop 38
* CEs [50,51] --> Loop 39
* CEs [49] --> Loop 40
* CEs [47,48] --> Loop 41
* CEs [46] --> Loop 42
* CEs [43] --> Loop 43
* CEs [41] --> Loop 44
* CEs [39] --> Loop 45
* CEs [37] --> Loop 46
* CEs [42] --> Loop 47
* CEs [40] --> Loop 48
* CEs [38] --> Loop 49
* CEs [36] --> Loop 50
* CEs [45] --> Loop 51
* CEs [44] --> Loop 52

### Ranking functions of CR cond2(V,V1,V2,V3,Out)
* RF of phase [43]: [V1,V2-1,V2-V3]
* RF of phase [45]: [V1,V2]
* RF of phase [47]: [V2-1,V2-V3]
* RF of phase [49]: [V2]

#### Partial ranking functions of CR cond2(V,V1,V2,V3,Out)
* Partial RF of phase [43]:
- RF of loop [43:1]:
V1
V2-1
V2-V3
* Partial RF of phase [45]:
- RF of loop [45:1]:
V1
V2
* Partial RF of phase [47]:
- RF of loop [47:1]:
V2-1
V2-V3
* Partial RF of phase [49]:
- RF of loop [49:1]:
V2


### Specialization of cost equations start/4
* CE 2 is refined into CE [64]
* CE 3 is refined into CE [65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92]
* CE 4 is refined into CE [93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140]
* CE 5 is refined into CE [141,142,143,144]
* CE 6 is refined into CE [145,146]
* CE 7 is refined into CE [147,148,149,150,151,152]
* CE 8 is refined into CE [153,154,155]


### Cost equations --> "Loop" of start/4
* CEs [92,140] --> Loop 53
* CEs [91,139] --> Loop 54
* CEs [137] --> Loop 55
* CEs [78] --> Loop 56
* CEs [76,136] --> Loop 57
* CEs [90,135] --> Loop 58
* CEs [89,134] --> Loop 59
* CEs [88,133] --> Loop 60
* CEs [87,132] --> Loop 61
* CEs [86,131] --> Loop 62
* CEs [75,130] --> Loop 63
* CEs [85,129] --> Loop 64
* CEs [84,128] --> Loop 65
* CEs [83,127] --> Loop 66
* CEs [82,126] --> Loop 67
* CEs [81,125] --> Loop 68
* CEs [73,124] --> Loop 69
* CEs [72,123] --> Loop 70
* CEs [71,122] --> Loop 71
* CEs [70,121] --> Loop 72
* CEs [77,120,138] --> Loop 73
* CEs [119] --> Loop 74
* CEs [68,118] --> Loop 75
* CEs [117] --> Loop 76
* CEs [67] --> Loop 77
* CEs [66,116] --> Loop 78
* CEs [113,114,115,152,154] --> Loop 79
* CEs [80,112] --> Loop 80
* CEs [79,110] --> Loop 81
* CEs [69,109,143,144,146,150,151] --> Loop 82
* CEs [64,74,108,111] --> Loop 83
* CEs [65,107,142,149,155] --> Loop 84
* CEs [93,94,95,96,97,98,99,100,101,102,103,104,105,106,141,145,147,148,153] --> Loop 85

### Ranking functions of CR start(V,V1,V2,V3)

#### Partial ranking functions of CR start(V,V1,V2,V3)


Computing Bounds
=====================================

#### Cost of chains of and(V,V1,Out):
* Chain [19]: 1
with precondition: [V=0,Out=0,V1>=0]

* Chain [18]: 1
with precondition: [V=1,V1=1,Out=1]

* Chain [17]: 1
with precondition: [V1=0,Out=0,V>=0]


#### Cost of chains of eq(V,V1,Out):
* Chain [[23],22]: 1*it(23)+1
Such that:it(23) =< V

with precondition: [Out=1,V=V1,V>=1]

* Chain [[23],21]: 1*it(23)+1
Such that:it(23) =< V

with precondition: [Out=0,V>=1,V1>=V+1]

* Chain [[23],20]: 1*it(23)+1
Such that:it(23) =< V1

with precondition: [Out=0,V1>=1,V>=V1+1]

* Chain [22]: 1
with precondition: [V=0,V1=0,Out=1]

* Chain [21]: 1
with precondition: [V=0,Out=0,V1>=1]

* Chain [20]: 1
with precondition: [V1=0,Out=0,V>=1]


#### Cost of chains of gr(V,V1,Out):
* Chain [[26],25]: 1*it(26)+1
Such that:it(26) =< V

with precondition: [Out=0,V>=1,V1>=V]

* Chain [[26],24]: 1*it(26)+1
Such that:it(26) =< V1

with precondition: [Out=1,V1>=1,V>=V1+1]

* Chain [25]: 1
with precondition: [V=0,Out=0,V1>=0]

* Chain [24]: 1
with precondition: [V1=0,Out=1,V>=1]


#### Cost of chains of p(V,Out):
* Chain [28]: 1
with precondition: [V=0,Out=0]

* Chain [27]: 1
with precondition: [V=Out+1,V>=1]


#### Cost of chains of cond2(V,V1,V2,V3,Out):
* Chain [[49],50,42]: 4*it(49)+8
Such that:it(49) =< V2

with precondition: [V=1,V1=0,V3=0,Out=0,V2>=1]

* Chain [[47],48,42]: 4*it(47)+1*s(1)+1*s(4)+8
Such that:it(47) =< V2
aux(2) =< 1
s(1) =< aux(2)
s(4) =< it(47)*aux(2)

with precondition: [V=1,V1=0,V3=1,Out=0,V2>=2]

* Chain [[47],48,41]: 4*it(47)+1*s(1)+1*s(4)+8
Such that:it(47) =< V2-V3
aux(3) =< V3
s(1) =< aux(3)
s(4) =< it(47)*aux(3)

with precondition: [V=1,V1=0,Out=0,V3>=2,V2>=V3+1]

* Chain [[45],[49],50,42]: 4*it(45)+4*it(49)+8
Such that:it(49) =< -V1+V2
it(45) =< V1

with precondition: [V=1,V3=0,Out=0,V1>=1,V2>=V1+1]

* Chain [[45],50,42]: 4*it(45)+8
Such that:it(45) =< V1

with precondition: [V=1,V3=0,Out=0,V1=V2,V1>=1]

* Chain [[45],46,42]: 4*it(45)+8
Such that:it(45) =< V1

with precondition: [V=1,V3=0,Out=0,V1=V2+1,V1>=2]

* Chain [[45],46,40]: 4*it(45)+8
Such that:it(45) =< V2

with precondition: [V=1,V3=0,Out=0,V2>=1,V1>=V2+2]

* Chain [[43],[47],48,42]: 4*it(43)+4*it(47)+1*s(1)+1*s(4)+1*s(7)+8
Such that:it(47) =< -V1+V2
it(43) =< V1
aux(5) =< 1
s(1) =< aux(5)
s(4) =< it(47)*aux(5)
s(7) =< it(43)*aux(5)

with precondition: [V=1,V3=1,Out=0,V1>=1,V2>=V1+2]

* Chain [[43],[47],48,41]: 4*it(43)+4*it(47)+1*s(1)+1*s(4)+1*s(7)+8
Such that:it(47) =< -V1+V2-V3
it(43) =< V1
aux(6) =< V3
s(1) =< aux(6)
s(4) =< it(47)*aux(6)
s(7) =< it(43)*aux(6)

with precondition: [V=1,Out=0,V1>=1,V3>=2,V2>=V1+V3+1]

* Chain [[43],48,42]: 4*it(43)+1*s(1)+1*s(7)+8
Such that:it(43) =< V2
aux(7) =< 1
s(1) =< aux(7)
s(7) =< it(43)*aux(7)

with precondition: [V=1,V3=1,Out=0,V1+1=V2,V1>=1]

* Chain [[43],48,41]: 4*it(43)+1*s(1)+1*s(7)+8
Such that:it(43) =< V2-V3
aux(8) =< V3
s(1) =< aux(8)
s(7) =< it(43)*aux(8)

with precondition: [V=1,Out=0,V1+V3=V2,V1>=1,V2>=V1+2]

* Chain [[43],44,42]: 4*it(43)+1*s(7)+1*s(8)+8
Such that:it(43) =< V2
aux(9) =< 1
s(8) =< aux(9)
s(7) =< it(43)*aux(9)

with precondition: [V=1,V3=1,Out=0,V1=V2,V1>=2]

* Chain [[43],44,41]: 4*it(43)+1*s(7)+1*s(8)+8
Such that:it(43) =< V2-V3
aux(10) =< V3
s(8) =< aux(10)
s(7) =< it(43)*aux(10)

with precondition: [V=1,Out=0,V1+V3=V2+1,V1>=2,V2>=V1+1]

* Chain [[43],44,39]: 4*it(43)+1*s(7)+1*s(8)+2*s(9)+8
Such that:aux(11) =< 2
it(43) =< V2
aux(12) =< 1
s(8) =< aux(12)
s(9) =< aux(11)
s(7) =< it(43)*aux(12)

with precondition: [V=1,V3=1,Out=0,V1=V2+1,V1>=3]

* Chain [[43],44,38]: 4*it(43)+1*s(7)+2*s(8)+8
Such that:it(43) =< V2
aux(13) =< 1
s(8) =< aux(13)
s(7) =< it(43)*aux(13)

with precondition: [V=1,V3=1,Out=0,V2>=2,V1>=V2+2]

* Chain [[43],44,34]: 4*it(43)+1*s(7)+3*s(8)+8
Such that:it(43) =< V2-V3
aux(16) =< V3
s(8) =< aux(16)
s(7) =< it(43)*aux(16)

with precondition: [V=1,Out=0,V1=V2,V3>=2,V1>=V3+1]

* Chain [[43],44,32]: 4*it(43)+1*s(7)+1*s(8)+4*s(14)+8
Such that:aux(19) =< V1-V2+V3
it(43) =< V2-V3
aux(20) =< V3
s(8) =< aux(20)
s(14) =< aux(19)
s(7) =< it(43)*aux(20)

with precondition: [V=1,Out=0,V2>=V1+1,V2>=V3+1,V1+V3>=V2+2]

* Chain [[43],44,31]: 4*it(43)+1*s(7)+3*s(8)+8
Such that:it(43) =< V2-V3
aux(22) =< V3
s(8) =< aux(22)
s(7) =< it(43)*aux(22)

with precondition: [V=1,Out=0,V3>=2,V1>=V2+2,V2>=V3+1]

* Chain [[43],44,30]: 4*it(43)+1*s(7)+3*s(8)+2*s(21)+8
Such that:it(43) =< V2-V3
aux(23) =< V3+1
aux(26) =< V3
s(8) =< aux(26)
s(21) =< aux(23)
s(7) =< it(43)*aux(26)

with precondition: [V=1,Out=0,V1=V2+1,V3>=2,V1>=V3+2]

* Chain [52,[45],50,42]: 5*it(45)+14
Such that:aux(27) =< V1
it(45) =< aux(27)

with precondition: [V=0,V3=0,Out=0,V1=V2,V1>=1]

* Chain [51,[43],44,42]: 5*it(43)+1*s(7)+3*s(8)+14
Such that:aux(29) =< 1
aux(30) =< V2
it(43) =< aux(30)
s(8) =< aux(29)
s(7) =< it(43)*aux(29)

with precondition: [V=0,V3=1,Out=0,V1=V2,V1>=2]

* Chain [51,[43],44,34]: 4*it(43)+1*s(7)+5*s(8)+1*s(25)+14
Such that:s(25) =< V2
it(43) =< V2-V3
aux(31) =< V3
s(8) =< aux(31)
s(7) =< it(43)*aux(31)

with precondition: [V=0,Out=0,V1=V2,V3>=2,V1>=V3+1]

* Chain [50,42]: 8
with precondition: [V=1,V1=0,V2=0,Out=0,V3>=0]

* Chain [48,42]: 1*s(1)+8
Such that:s(1) =< 1

with precondition: [V=1,V1=0,V2=1,Out=0,V3>=1]

* Chain [48,41]: 1*s(1)+8
Such that:s(1) =< V2

with precondition: [V=1,V1=0,Out=0,V2>=2,V3>=V2]

* Chain [46,42]: 8
with precondition: [V=1,V1=1,V2=0,Out=0,V3>=0]

* Chain [46,40]: 8
with precondition: [V=1,V2=0,V3=0,Out=0,V1>=2]

* Chain [46,39]: 2*s(9)+8
Such that:aux(11) =< V1
s(9) =< aux(11)

with precondition: [V=1,V2=0,Out=0,V1>=2,V3+1>=V1]

* Chain [46,38]: 1*s(11)+8
Such that:s(11) =< V3

with precondition: [V=1,V2=0,Out=0,V3>=1,V1>=V3+2]

* Chain [44,42]: 1*s(8)+8
Such that:s(8) =< 1

with precondition: [V=1,V1=1,V2=1,Out=0,V3>=1]

* Chain [44,41]: 1*s(8)+8
Such that:s(8) =< V2

with precondition: [V=1,V1=1,Out=0,V2>=2,V3>=V2]

* Chain [44,39]: 1*s(8)+2*s(9)+8
Such that:s(8) =< 1
aux(11) =< V1
s(9) =< aux(11)

with precondition: [V=1,V2=1,Out=0,V1>=2,V3+1>=V1]

* Chain [44,38]: 1*s(8)+1*s(11)+8
Such that:s(8) =< 1
s(11) =< V3

with precondition: [V=1,V2=1,Out=0,V3>=1,V1>=V3+2]

* Chain [44,34]: 3*s(8)+8
Such that:aux(15) =< V2
s(8) =< aux(15)

with precondition: [V=1,Out=0,V1=V2,V1>=2,V3>=V1]

* Chain [44,32]: 1*s(8)+4*s(14)+8
Such that:aux(19) =< V1
s(8) =< V2
s(14) =< aux(19)

with precondition: [V=1,Out=0,V1>=2,V2>=V1+1,V3>=V2]

* Chain [44,31]: 2*s(8)+1*s(19)+8
Such that:s(19) =< V3
aux(21) =< V2
s(8) =< aux(21)

with precondition: [V=1,Out=0,V2>=2,V3>=V2,V1>=V3+2]

* Chain [44,30]: 3*s(8)+2*s(21)+8
Such that:aux(23) =< V1
aux(25) =< V2
s(8) =< aux(25)
s(21) =< aux(23)

with precondition: [V=1,Out=0,V2>=2,V3+1>=V1,V1>=V2+1]

* Chain [42]: 4
with precondition: [V=0,V1=0,V2=0,Out=0,V3>=0]

* Chain [41]: 4
with precondition: [V=0,V1=0,Out=0,V2>=1,V3>=0]

* Chain [40]: 4
with precondition: [V=0,V2=0,V3=0,Out=0,V1>=1]

* Chain [39]: 2*s(9)+4
Such that:aux(11) =< V1
s(9) =< aux(11)

with precondition: [V=0,V2=0,Out=0,V1>=1,V3>=V1]

* Chain [38]: 1*s(11)+4
Such that:s(11) =< V3

with precondition: [V=0,V2=0,Out=0,V3>=1,V1>=V3+1]

* Chain [37]: 1*s(28)+4
Such that:s(28) =< V1

with precondition: [V=0,V3=0,Out=0,V1=V2,V1>=1]

* Chain [36]: 1*s(29)+4
Such that:s(29) =< V1

with precondition: [V=0,V3=0,Out=0,V1>=1,V2>=V1+1]

* Chain [35]: 1*s(30)+4
Such that:s(30) =< V2

with precondition: [V=0,V3=0,Out=0,V2>=1,V1>=V2+1]

* Chain [34]: 2*s(12)+4
Such that:aux(14) =< V1
s(12) =< aux(14)

with precondition: [V=0,Out=0,V1=V2,V1>=1,V3>=V1]

* Chain [33]: 1*s(31)+1*s(32)+4
Such that:s(31) =< V2
s(32) =< V3

with precondition: [V=0,Out=0,V1=V2,V3>=1,V1>=V3+1]

* Chain [32]: 4*s(14)+4
Such that:aux(19) =< V1
s(14) =< aux(19)

with precondition: [V=0,Out=0,V1>=1,V2>=V1+1,V3>=V1]

* Chain [31]: 1*s(18)+1*s(19)+4
Such that:s(18) =< V2
s(19) =< V3

with precondition: [V=0,Out=0,V2>=1,V3>=1,V1>=V2+1,V1>=V3+1]

* Chain [30]: 2*s(20)+2*s(21)+4
Such that:aux(23) =< V1
aux(24) =< V2
s(21) =< aux(23)
s(20) =< aux(24)

with precondition: [V=0,Out=0,V2>=1,V3>=V1,V1>=V2+1]

* Chain [29]: 1*s(33)+1*s(34)+4
Such that:s(33) =< V1
s(34) =< V3

with precondition: [V=0,Out=0,V3>=1,V2>=V1+1,V1>=V3+1]


#### Cost of chains of start(V,V1,V2,V3):
* Chain [85]: 16*s(51)+9*s(52)+13*s(56)+4*s(58)+3*s(63)+1*s(64)+1*s(65)+14
Such that:s(57) =< 1
s(58) =< V2-V3
aux(35) =< V1
aux(36) =< V2
aux(37) =< V3
s(51) =< aux(35)
s(56) =< aux(36)
s(52) =< aux(37)
s(63) =< s(57)
s(64) =< s(56)*s(57)
s(65) =< s(58)*aux(37)

with precondition: [V=0]

* Chain [84]: 8
with precondition: [V1=0,V>=0]

* Chain [83]: 2*s(78)+1*s(79)+8
Such that:s(79) =< 1
aux(38) =< V2
s(78) =< aux(38)

with precondition: [V>=0,V1>=0,V2>=0,V3>=0]

* Chain [82]: 8*s(81)+2*s(83)+2*s(84)+10
Such that:aux(39) =< V
aux(40) =< V1
aux(41) =< V2
s(83) =< aux(39)
s(84) =< aux(40)
s(81) =< aux(41)

with precondition: [V>=1]

* Chain [81]: 3*s(87)+8*s(88)+2*s(91)+10
Such that:aux(43) =< 1
aux(44) =< V2
s(88) =< aux(44)
s(87) =< aux(43)
s(91) =< s(88)*aux(43)

with precondition: [V=1,V1=0,V3=1,V2>=2]

* Chain [80]: 3*s(96)+8*s(97)+2*s(100)+10
Such that:aux(46) =< V2-V3
aux(47) =< V3
s(97) =< aux(46)
s(96) =< aux(47)
s(100) =< s(97)*aux(47)

with precondition: [V=1,V1=0,V3>=2,V2>=V3+1]

* Chain [79]: 1*s(105)+1*s(106)+1*s(107)+8
Such that:s(105) =< 1
s(107) =< V1
s(106) =< V2

with precondition: [V=V1,V>=1]

* Chain [78]: 8
with precondition: [V=1,V2=0,V3=0,V1>=1]

* Chain [77]: 2*s(109)+6
Such that:s(108) =< V1
s(109) =< s(108)

with precondition: [V=1,V2=0,V1>=1,V3>=V1]

* Chain [76]: 2*s(111)+8
Such that:s(110) =< V1
s(111) =< s(110)

with precondition: [V=1,V2=0,V1>=2,V3+1>=V1]

* Chain [75]: 2*s(112)+8
Such that:aux(48) =< V3
s(112) =< aux(48)

with precondition: [V=1,V2=0,V3>=1,V1>=V3+1]

* Chain [74]: 1*s(114)+2*s(116)+8
Such that:s(114) =< 1
s(115) =< V1
s(116) =< s(115)

with precondition: [V=1,V2=1,V1>=2,V3+1>=V1]

* Chain [73]: 4*s(117)+3*s(119)+1*s(120)+8
Such that:s(120) =< 1
aux(50) =< V2
aux(51) =< V3
s(119) =< aux(51)
s(117) =< aux(50)

with precondition: [V=1,V2>=1,V3>=V2,V1>=V3+1]

* Chain [72]: 8*s(125)+10
Such that:aux(52) =< V1
s(125) =< aux(52)

with precondition: [V=1,V3=0,V1=V2,V1>=1]

* Chain [71]: 8*s(127)+10
Such that:aux(53) =< V1
s(127) =< aux(53)

with precondition: [V=1,V3=0,V1=V2+1,V1>=2]

* Chain [70]: 8*s(129)+8*s(130)+10
Such that:aux(54) =< -V1+V2
aux(55) =< V1
s(129) =< aux(54)
s(130) =< aux(55)

with precondition: [V=1,V3=0,V1>=1,V2>=V1+1]

* Chain [69]: 8*s(133)+10
Such that:aux(56) =< V2
s(133) =< aux(56)

with precondition: [V=1,V3=0,V2>=1,V1>=V2+2]

* Chain [68]: 3*s(135)+8*s(136)+2*s(139)+10
Such that:aux(58) =< 1
aux(59) =< V2
s(136) =< aux(59)
s(135) =< aux(58)
s(139) =< s(136)*aux(58)

with precondition: [V=1,V3=1,V1+1=V2,V1>=1]

* Chain [67]: 3*s(144)+8*s(145)+2*s(148)+10
Such that:aux(61) =< 1
aux(62) =< V2
s(145) =< aux(62)
s(144) =< aux(61)
s(148) =< s(145)*aux(61)

with precondition: [V=1,V3=1,V1=V2,V1>=2]

* Chain [66]: 3*s(153)+4*s(155)+4*s(158)+1*s(159)+4*s(161)+1*s(165)+10
Such that:s(155) =< V1
s(161) =< V2
aux(64) =< 1
aux(65) =< 2
s(153) =< aux(64)
s(158) =< aux(65)
s(165) =< s(161)*aux(64)
s(159) =< s(155)*aux(64)

with precondition: [V=1,V3=1,V1=V2+1,V1>=3]

* Chain [65]: 3*s(166)+8*s(167)+8*s(168)+2*s(171)+2*s(172)+10
Such that:aux(67) =< 1
aux(68) =< -V1+V2
aux(69) =< V1
s(167) =< aux(68)
s(168) =< aux(69)
s(166) =< aux(67)
s(171) =< s(167)*aux(67)
s(172) =< s(168)*aux(67)

with precondition: [V=1,V3=1,V1>=1,V2>=V1+2]

* Chain [64]: 5*s(179)+8*s(180)+2*s(183)+10
Such that:aux(71) =< 1
aux(72) =< V2
s(180) =< aux(72)
s(179) =< aux(71)
s(183) =< s(180)*aux(71)

with precondition: [V=1,V3=1,V2>=2,V1>=V2+2]

* Chain [63]: 3*s(188)+3*s(192)+8
Such that:aux(73) =< V1
s(191) =< V2
s(188) =< aux(73)
s(192) =< s(191)

with precondition: [V=1,V1=V2,V1>=1,V3>=V1]

* Chain [62]: 7*s(193)+4*s(194)+1*s(197)+4*s(198)+1*s(201)+10
Such that:s(198) =< V1-V3
s(194) =< V2-V3
aux(75) =< V3
s(193) =< aux(75)
s(201) =< s(198)*aux(75)
s(197) =< s(194)*aux(75)

with precondition: [V=1,V1=V2,V3>=2,V1>=V3+1]

* Chain [61]: 7*s(202)+8*s(203)+4*s(207)+2*s(208)+10
Such that:aux(77) =< V2-V3
aux(78) =< V3
aux(79) =< V3+1
s(203) =< aux(77)
s(202) =< aux(78)
s(207) =< aux(79)
s(208) =< s(203)*aux(78)

with precondition: [V=1,V1=V2+1,V3>=2,V1>=V3+2]

* Chain [60]: 3*s(215)+4*s(216)+1*s(219)+4*s(220)+1*s(223)+10
Such that:s(220) =< V1
s(216) =< V2-V3
aux(81) =< V3
s(215) =< aux(81)
s(223) =< s(220)*aux(81)
s(219) =< s(216)*aux(81)

with precondition: [V=1,V2=V1+V3,V1>=1,V2>=V1+2]

* Chain [59]: 3*s(224)+4*s(225)+1*s(228)+4*s(229)+1*s(232)+10
Such that:s(229) =< V1
s(225) =< V2-V3
aux(83) =< V3
s(224) =< aux(83)
s(232) =< s(229)*aux(83)
s(228) =< s(225)*aux(83)

with precondition: [V=1,V2+1=V1+V3,V1>=2,V2>=V1+1]

* Chain [58]: 3*s(233)+8*s(234)+8*s(235)+2*s(238)+2*s(239)+10
Such that:aux(85) =< -V1+V2-V3
aux(86) =< V1
aux(87) =< V3
s(234) =< aux(85)
s(235) =< aux(86)
s(233) =< aux(87)
s(238) =< s(234)*aux(87)
s(239) =< s(235)*aux(87)

with precondition: [V=1,V1>=1,V3>=2,V2>=V1+V3+1]

* Chain [57]: 2*s(246)+8*s(248)+8
Such that:aux(88) =< V1
aux(89) =< V2
s(246) =< aux(89)
s(248) =< aux(88)

with precondition: [V=1,V1>=1,V2>=V1+1,V3>=V2]

* Chain [56]: 3*s(252)+2*s(255)+6
Such that:s(253) =< V1
aux(90) =< V2
s(252) =< aux(90)
s(255) =< s(253)

with precondition: [V=1,V2>=1,V3>=V1,V1>=V2+1]

* Chain [55]: 3*s(259)+2*s(260)+8
Such that:s(257) =< V1
s(258) =< V2
s(259) =< s(258)
s(260) =< s(257)

with precondition: [V=1,V2>=2,V3+1>=V1,V1>=V2+1]

* Chain [54]: 7*s(261)+8*s(262)+2*s(265)+10
Such that:aux(92) =< V2-V3
aux(93) =< V3
s(262) =< aux(92)
s(261) =< aux(93)
s(265) =< s(262)*aux(93)

with precondition: [V=1,V3>=2,V1>=V2+2,V2>=V3+1]

* Chain [53]: 3*s(270)+8*s(272)+8*s(275)+2*s(276)+10
Such that:aux(95) =< V1-V2+V3
aux(96) =< V2-V3
aux(97) =< V3
s(272) =< aux(96)
s(270) =< aux(97)
s(275) =< aux(95)
s(276) =< s(272)*aux(97)

with precondition: [V=1,V2>=V1+1,V2>=V3+1,V1+V3>=V2+2]


Closed-form bounds of start(V,V1,V2,V3):
-------------------------------------
* Chain [85] with precondition: [V=0]
- Upper bound: nat(V1)*16+17+nat(V2)*14+nat(V3)*9+nat(V2-V3)*nat(V3)+nat(V2-V3)*4
- Complexity: n^2
* Chain [84] with precondition: [V1=0,V>=0]
- Upper bound: 8
- Complexity: constant
* Chain [83] with precondition: [V>=0,V1>=0,V2>=0,V3>=0]
- Upper bound: 2*V2+9
- Complexity: n
* Chain [82] with precondition: [V>=1]
- Upper bound: 2*V+10+nat(V1)*2+nat(V2)*8
- Complexity: n
* Chain [81] with precondition: [V=1,V1=0,V3=1,V2>=2]
- Upper bound: 10*V2+13
- Complexity: n
* Chain [80] with precondition: [V=1,V1=0,V3>=2,V2>=V3+1]
- Upper bound: 8*V2-8*V3+ (3*V3+10+ (V2-V3)* (2*V3))
- Complexity: n^2
* Chain [79] with precondition: [V=V1,V>=1]
- Upper bound: V1+9+nat(V2)
- Complexity: n
* Chain [78] with precondition: [V=1,V2=0,V3=0,V1>=1]
- Upper bound: 8
- Complexity: constant
* Chain [77] with precondition: [V=1,V2=0,V1>=1,V3>=V1]
- Upper bound: 2*V1+6
- Complexity: n
* Chain [76] with precondition: [V=1,V2=0,V1>=2,V3+1>=V1]
- Upper bound: 2*V1+8
- Complexity: n
* Chain [75] with precondition: [V=1,V2=0,V3>=1,V1>=V3+1]
- Upper bound: 2*V3+8
- Complexity: n
* Chain [74] with precondition: [V=1,V2=1,V1>=2,V3+1>=V1]
- Upper bound: 2*V1+9
- Complexity: n
* Chain [73] with precondition: [V=1,V2>=1,V3>=V2,V1>=V3+1]
- Upper bound: 4*V2+3*V3+9
- Complexity: n
* Chain [72] with precondition: [V=1,V3=0,V1=V2,V1>=1]
- Upper bound: 8*V1+10
- Complexity: n
* Chain [71] with precondition: [V=1,V3=0,V1=V2+1,V1>=2]
- Upper bound: 8*V1+10
- Complexity: n
* Chain [70] with precondition: [V=1,V3=0,V1>=1,V2>=V1+1]
- Upper bound: 8*V2+10
- Complexity: n
* Chain [69] with precondition: [V=1,V3=0,V2>=1,V1>=V2+2]
- Upper bound: 8*V2+10
- Complexity: n
* Chain [68] with precondition: [V=1,V3=1,V1+1=V2,V1>=1]
- Upper bound: 10*V2+13
- Complexity: n
* Chain [67] with precondition: [V=1,V3=1,V1=V2,V1>=2]
- Upper bound: 10*V2+13
- Complexity: n
* Chain [66] with precondition: [V=1,V3=1,V1=V2+1,V1>=3]
- Upper bound: 5*V1+5*V2+21
- Complexity: n
* Chain [65] with precondition: [V=1,V3=1,V1>=1,V2>=V1+2]
- Upper bound: 10*V2+13
- Complexity: n
* Chain [64] with precondition: [V=1,V3=1,V2>=2,V1>=V2+2]
- Upper bound: 10*V2+15
- Complexity: n
* Chain [63] with precondition: [V=1,V1=V2,V1>=1,V3>=V1]
- Upper bound: 3*V1+3*V2+8
- Complexity: n
* Chain [62] with precondition: [V=1,V1=V2,V3>=2,V1>=V3+1]
- Upper bound: 4*V2-4*V3+ (4*V1-4*V3+ (7*V3+10+ (V1-V3)*V3+ (V2-V3)*V3))
- Complexity: n^2
* Chain [61] with precondition: [V=1,V1=V2+1,V3>=2,V1>=V3+2]
- Upper bound: 8*V2-8*V3+ (7*V3+10+ (V2-V3)* (2*V3)+ (4*V3+4))
- Complexity: n^2
* Chain [60] with precondition: [V=1,V2=V1+V3,V1>=1,V2>=V1+2]
- Upper bound: 4*V2-4*V3+ (4*V1+10+V3*V1+3*V3+ (V2-V3)*V3)
- Complexity: n^2
* Chain [59] with precondition: [V=1,V2+1=V1+V3,V1>=2,V2>=V1+1]
- Upper bound: 4*V2-4*V3+ (4*V1+10+V3*V1+3*V3+ (V2-V3)*V3)
- Complexity: n^2
* Chain [58] with precondition: [V=1,V1>=1,V3>=2,V2>=V1+V3+1]
- Upper bound: -8*V1+8*V2-8*V3+ (8*V1+3*V3+10+2*V3*V1+ (-V1+V2-V3)* (2*V3))
- Complexity: n^2
* Chain [57] with precondition: [V=1,V1>=1,V2>=V1+1,V3>=V2]
- Upper bound: 8*V1+2*V2+8
- Complexity: n
* Chain [56] with precondition: [V=1,V2>=1,V3>=V1,V1>=V2+1]
- Upper bound: 2*V1+3*V2+6
- Complexity: n
* Chain [55] with precondition: [V=1,V2>=2,V3+1>=V1,V1>=V2+1]
- Upper bound: 2*V1+3*V2+8
- Complexity: n
* Chain [54] with precondition: [V=1,V3>=2,V1>=V2+2,V2>=V3+1]
- Upper bound: 8*V2-8*V3+ (7*V3+10+ (V2-V3)* (2*V3))
- Complexity: n^2
* Chain [53] with precondition: [V=1,V2>=V1+1,V2>=V3+1,V1+V3>=V2+2]
- Upper bound: 8*V2-8*V3+ (8*V1-8*V2+8*V3+ (3*V3+10+ (V2-V3)* (2*V3)))
- Complexity: n^2

### Maximum cost of start(V,V1,V2,V3): max([max([nat(V3)+1+max([nat(V2)*4,nat(V2-V3)*nat(V3)+1+nat(V2-V3)*4+max([nat(V1-V3)*nat(V3)+nat(V3)*4+nat(V1-V3)*4,nat(V2-V3)*nat(V3)+nat(V2-V3)*4+max([nat(V1-V2+V3)*8,nat(V3+1)*4+nat(V3)*4])])])+nat(V3)*2,nat(V2)*6+1+ (nat(V2)*2+5)+ (nat(V2)*2+1)])+2,nat(V1)+max([nat(V1)+max([max([3,nat(V2)*3+max([2,2*V+4+nat(V2)*5])]),nat(V1)+2+max([nat(V2)*3,nat(V1)+max([nat(V1)+max([nat(V1)*3+max([max([2,nat(V2)*2,nat(-V1+V2)*8+2,nat(V3)*3+2+nat(V3)*2*nat(V1)+nat(V3)*2*nat(-V1+V2-V3)+nat(-V1+V2-V3)*8]),nat(V1)*2+5+max([nat(-V1+V2)*10,nat(V1)*6+4+nat(V2)*14+nat(V3)*9+nat(V2-V3)*nat(V3)+nat(V2-V3)*4])]),nat(V2)*5+13]),nat(V3)*nat(V1)+2+nat(V3)*3+nat(V2-V3)*nat(V3)+nat(V2-V3)*4])])]),nat(V2)+3])])+6
Asymptotic class: n^2
* Total analysis performed in 1762 ms.

(10) BOUNDS(1, n^2)